The present invention is related to techniques for formal analysis and verification of software.
Model checking is an automatic technique for the verification of concurrent systems. It has several advantages over simulation, testing, and deductive reasoning, and has been used successfully in practice to verify complex sequential circuit designs and communication protocols. See E. M. Clarke, O. Grumberg, and D. A. Peled, “Model Checking,” MIT Press, 2000. In particular, model checking is automatic, and, if the design contains an error, model checking produces a counter-example (i.e., a witness of the offending behavior of the system) that can be used for effective debugging of the system. While symbolic model checking using binary decision diagrams (BDDs) offer the potential of exhaustive coverage of large state-spaces, it often does not scale well enough in practice. An alternative approach is bounded model checking (BMC) focusing on the search for counter-examples of bounded length only. See A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs,” Proc. of the 36th ACM/IEEE Design Automation Conference, pp. 317-20 (1999). Effectively, the problem is translated to a Boolean formula, such that the formula is satisfiable if and only if there exists a counter-example of length k. In practice, k can be increased incrementally starting from one to find a shortest counter-example if one exists. However, additional reasoning is needed to ensure completeness of the verification when no counter-example exists. The satisfiability check in the BMC approach is typically performed by what is known as a back-end SAT-solver. See, e.g., M. K. Ganai, L. Zhang, P. Ashar, and A. Gupta, “Combining strength of circuit-based and CNF-based algorithms for a high performance SAT solver,” in Design Automation Conference, 2002; E. Goldberg and Y. Novikov, “Berkmin: A fast and robust SAT solver,” in Design Automation and Test in Europe, pages 132-39, 2002; J. P. Marques-Silva and K. A. Sakallah, “GRASP: A search algorithm for prepositional satisfiability,” IEEE Transactions on Computers, 48: 506-21, 1999; and M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Enginnering an efficient SAT solver,” in Design Automation Conference, 2001.
Recently, it has been proposed to apply bounded model checking techniques to the formal verification of software such as C programs. See E. Clarke, D. Kroening, “Hardware Verification using ANSI-C Programs as a Reference,” Proceedings of ASP-DAC 2003, pp. 308-11 (January 2003). In this approach, a C program is translated into a monolithic SAT formula, namely a bit vector equation, which is then used with SAT-based bounded model checking to check consistency properties, including checking the equivalence of the C program to a register-transfer level (RTL) hardware design. Each individual statement in the C program is considered to be an atomic component of the program. Unfortunately, this statement-based approach has limitations in terms of concisely handling loops and functions and does not take full advantage of recent advances in model checking.